ds:x:Id fp Type, da:a:Knd fp Type, init:x:Id fp ds(x)?Void, pre:a:Id fp State(ds),
ef:kx::Knd  Id fp State(ds)Valtype(da;kx.1)ds(kx.2)?Void,
send:kl::Knd  IdLnk fp
send:(tg:Id  (State(ds)Valtype(da;kl.1)(da(rcv(kl.2,tg))?Void List))) List,
frame:x:Id fp Knd List, sframe:ltg::IdLnk  Id fp Knd List, aframe:k:Knd fp Id List,
bframe:k:Knd fp IdLnk List, rframe:x:Id fp Knd List, prob:a:Id fp FinProbSpace.
ma{ds;
ma{da;
ma{init;
ma{pre;
ma{ef;
ma{send;
ma{frame;
ma{sframe;
ma{aframe;
ma{bframe;
ma{rframe;
ma{prob}
 MsgA 

latex

Definitions	Void, t  T, x:A.B(x), Top, x:A  B(x), Id, FinProbSpace, a:A fp B(a), Knd, type List, IdLnk, Type, x:A. B(x), x. t(x), t.2, rcv(l,tg), KindDeq, x.A(x), f(x)?z, t.1, Valtype(da;k), x:AB(x), State(ds), IdDeq, , , Unit, , <a, b>, mk-ma, MsgA
Lemmas	finite-prob-space wf, IdLnk wf, Knd wf, it wf, bool wf, rationals wf, Id wf, id-deq wf, fpf wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, top wf